EOrderAxioms(E;pred?;info)
== (e:E, l:IdLnk.
== e':E
== (e'':E. 
== (rcv?(e''))
==  (sender(e'') = e)
==  (link(e'') = l)
==  (((e'' = e')  e'' < e')  (loc(e') = destination(l)))))
==  (e,e':E. (loc(e) = loc(e'))  (pred?(e) = pred?(e'))  (e = e'))
==  SWellFounded(pred!(e;e'))
==  (e:E. ((first(e)))  (loc(pred(e)) = loc(e)))
==  (e:E. (rcv?(e))  (loc(sender(e)) = source(link(e))))
==  (e,e':E.
==  (rcv?(e))  (rcv?(e'))  (link(e) = link(e'))  sender(e) < sender(e')  e < e') 

latex

---

clarification:

EOrderAxioms{i:l}
EOrderAxioms(E; pred?; info)
== (e:E, l:IdLnk.
== e':E
== (e'':E. 
== (rcv?(info;e''))
==  (sender(info;e'') = e  E)
==  (link(info;e'') = l  IdLnk)
==  (((e'' = e'  E)  cless(E;pred?;info;e'';e'))  (loc(info;e') = destination(l)  Id))))
==  (e:E, e':E.
==  (loc(info;e) = loc(info;e')  Id)  (pred?(e) = pred?(e')  (E + Unit))  (e = e'  E))
==  strongwellfounded(E; e,e'.pred!(E;pred?;info;e;e'))
==  (e:E. ((first(pred?;e)))  (loc(info;pred(pred?;e)) = loc(info;e)  Id))
==  (e:E. (rcv?(info;e))  (loc(info;sender(info;e)) = source(link(info;e))  Id))
==  (e:E, e':E.
==  (rcv?(info;e))
==   (rcv?(info;e'))
==   (link(info;e) = link(info;e')  IdLnk)
==   cless(E;pred?;info;sender(info;e);sender(info;e'))
==   cless(E;pred?;info;e;e')) 

latex

Definitions	x:A. B(x), P  Q, destination(l), left + right, Unit, f(a), SWellFounded(R(x;y)), pred!(e;e'), A, first(e), pred(e), P  Q, Id, loc(e), source(l), x:A. B(x), b, rcv?(e), s = t, IdLnk, link(e), P  Q, sender(e), e < e'
FDL editor aliases	EOrderAxioms